Consider the TRS R consisting of the rewrite rules
1:
f(0,1,g(x,y),z)
→ f(g(x,y),g(x,y),g(x,y),h(x))
2:
g(0,1)
→ 0
3:
g(0,1)
→ 1
4:
h(g(x,y))
→ h(x)
There are 3 dependency pairs:
5:
F(0,1,g(x,y),z)
→ F(g(x,y),g(x,y),g(x,y),h(x))
6:
F(0,1,g(x,y),z)
→ H(x)
7:
H(g(x,y))
→ H(x)
The approximated dependency graph contains 2 SCCs:
{7}
and {5}.
Consider the SCC {7}.
There are no usable rules.
By taking the AF π with
π(H) = 1
and π(g) = [1] together with
the lexicographic path order with
empty precedence,
rule 7
is strictly decreasing.
Consider the SCC {5}.
The usable rules are {2-4}.
The constraints could not be solved.